/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓CS258␈↓ ¬vTying up a loose End␈↓ 
cWinter 1979


␈↓ α∧␈↓␈↓ αTThe following theorem ties up a loose end from the lecture of 13 February.

␈↓ α∧␈↓Theorem␈α
-␈α
Let␈α
␈↓↓D␈↓␈α
be␈α
partial␈α
ordered␈α
by␈α
<,␈α
and␈α
let␈α
<␈α
satisfy␈α
a␈α
descending␈α
chain␈α
condition,␈α
i.e.␈α
admit
␈↓ α∧␈↓a␈α∩course-of-values␈α∩induction␈α∩schema.␈α∩ Let␈α∪␈↓↓h: D → D␈↓␈α∩and␈α∩let␈α∩the␈α∩function␈α∩g␈α∪satisfy␈α∩␈↓↓g: D → D␈↓,
␈↓ α∧␈↓␈↓↓(∀x)(¬(x ε D) ⊃ ¬(g(x) ε D)␈↓␈α-and␈α.␈↓↓(∀x)(x ε D ⊃ g(x) > x)␈↓.␈α- Let␈α.the␈α-function␈α.␈↓↓f␈↓␈α-satisfy
␈↓ α∧␈↓␈↓↓(∀x)(x ε D ⊃ f(x) = g(f(h(x))))␈↓.  Then ␈↓↓(∀x)(x ε D ⊃ ¬(f(x) ε D))␈↓.

␈↓ α∧␈↓Proof - The course-of-values induction schema is

␈↓ α∧␈↓␈↓ αT␈↓↓(∀x)(x ε D ∧ (∀y)(y ε D ∧ y < x ⊃ ␈↓	F␈↓↓(y)) ⊃ ␈↓	F␈↓↓(x)) ⊃ (∀x)(x ε D ⊃ ␈↓	F␈↓↓(x))␈↓.

␈↓ α∧␈↓In that schema we take

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(x) ≡ (∀z)(z ε D ⊃ f(z) ≠ x)␈↓.

␈↓ α∧␈↓Now choose ␈↓↓x ε D␈↓, and suppose ␈↓↓f(z) = x␈↓ for some ␈↓↓z ε D␈↓.  We then have

␈↓ α∧␈↓␈↓ αT␈↓↓x = f(z) = g(f(h(z))) > f(h(z))␈↓,

␈↓ α∧␈↓and so by the induction hypothesis, ␈↓↓¬(f(h(z)) ε D)␈↓.  Hence by the properties of ␈↓↓g, ␈↓ ␈↓↓x = g(f(h(z)))␈↓

␈↓ α∧␈↓isn't in ␈↓↓D␈↓ either, which completes the induction. ␈↓π1␈↓.

␈↓ α∧␈↓␈↓ αTThe theorem shows the obvious facts that neither

␈↓ α∧␈↓␈↓↓P1: f(x) ← f(x␈↓#
2␈↓# + 1) + 1␈↓

␈↓ α∧␈↓nor

␈↓ α∧␈↓␈↓↓P2: f(x) ← ␈↓A␈↓↓.f(x.␈↓A␈↓↓)␈↓

␈↓ α∧␈↓terminates.␈α
 Of␈α∞course,␈α
the␈α
minimization␈α∞schema␈α
does␈α
it␈α∞more␈α
simply,␈α
but␈α∞the␈α
theorem␈α∞gives␈α
the
␈↓ α∧␈↓further␈α⊂fact␈α⊂that␈α⊂the␈α⊂functional␈α⊂equations␈α⊂have␈α⊂no␈α⊂solutions␈α⊂taking␈α⊂values␈α⊂among␈α⊃the␈α⊂natural
␈↓ α∧␈↓numbers or S-expressions respectively.